![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cbvrexf | Structured version Visualization version GIF version |
Description: Rule used to change bound variables, using implicit substitution. (Contributed by FL, 27-Apr-2008.) (Revised by Mario Carneiro, 9-Oct-2016.) |
Ref | Expression |
---|---|
cbvralf.1 | ⊢ Ⅎ𝑥𝐴 |
cbvralf.2 | ⊢ Ⅎ𝑦𝐴 |
cbvralf.3 | ⊢ Ⅎ𝑦𝜑 |
cbvralf.4 | ⊢ Ⅎ𝑥𝜓 |
cbvralf.5 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
cbvrexf | ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbvralf.1 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
2 | cbvralf.2 | . . . 4 ⊢ Ⅎ𝑦𝐴 | |
3 | cbvralf.3 | . . . . 5 ⊢ Ⅎ𝑦𝜑 | |
4 | 3 | nfn 1929 | . . . 4 ⊢ Ⅎ𝑦 ¬ 𝜑 |
5 | cbvralf.4 | . . . . 5 ⊢ Ⅎ𝑥𝜓 | |
6 | 5 | nfn 1929 | . . . 4 ⊢ Ⅎ𝑥 ¬ 𝜓 |
7 | cbvralf.5 | . . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
8 | 7 | notbid 307 | . . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓)) |
9 | 1, 2, 4, 6, 8 | cbvralf 3300 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑦 ∈ 𝐴 ¬ 𝜓) |
10 | 9 | notbii 309 | . 2 ⊢ (¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∀𝑦 ∈ 𝐴 ¬ 𝜓) |
11 | dfrex2 3130 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑) | |
12 | dfrex2 3130 | . 2 ⊢ (∃𝑦 ∈ 𝐴 𝜓 ↔ ¬ ∀𝑦 ∈ 𝐴 ¬ 𝜓) | |
13 | 10, 11, 12 | 3bitr4i 292 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 Ⅎwnf 1853 Ⅎwnfc 2885 ∀wral 3046 ∃wrex 3047 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1867 ax-4 1882 ax-5 1984 ax-6 2050 ax-7 2086 ax-10 2164 ax-11 2179 ax-12 2192 ax-13 2387 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1631 df-ex 1850 df-nf 1855 df-sb 2043 df-clel 2752 df-nfc 2887 df-ral 3051 df-rex 3052 |
This theorem is referenced by: cbvrex 3303 reusv2lem4 5017 reusv2 5019 nnwof 11943 cbviunf 29675 ac6sf2 29734 dfimafnf 29741 aciunf1lem 29767 bnj1400 31209 phpreu 33702 poimirlem26 33744 indexa 33837 evth2f 39669 fvelrnbf 39672 evthf 39681 eliin2f 39782 stoweidlem34 40750 ovnlerp 41278 |
Copyright terms: Public domain | W3C validator |