![]() |
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 1824 | . . . 4 ⊢ Ⅎ𝑦 ¬ 𝜑 |
5 | cbvralf.4 | . . . . 5 ⊢ Ⅎ𝑥𝜓 | |
6 | 5 | nfn 1824 | . . . 4 ⊢ Ⅎ𝑥 ¬ 𝜓 |
7 | cbvralf.5 | . . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
8 | 7 | notbid 307 | . . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓)) |
9 | 1, 2, 4, 6, 8 | cbvralf 3195 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑦 ∈ 𝐴 ¬ 𝜓) |
10 | 9 | notbii 309 | . 2 ⊢ (¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∀𝑦 ∈ 𝐴 ¬ 𝜓) |
11 | dfrex2 3025 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑) | |
12 | dfrex2 3025 | . 2 ⊢ (∃𝑦 ∈ 𝐴 𝜓 ↔ ¬ ∀𝑦 ∈ 𝐴 ¬ 𝜓) | |
13 | 10, 11, 12 | 3bitr4i 292 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 Ⅎwnf 1748 Ⅎwnfc 2780 ∀wral 2941 ∃wrex 2942 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-cleq 2644 df-clel 2647 df-nfc 2782 df-ral 2946 df-rex 2947 |
This theorem is referenced by: cbvrex 3198 reusv2lem4 4902 reusv2 4904 nnwof 11792 cbviunf 29498 ac6sf2 29557 dfimafnf 29564 aciunf1lem 29590 bnj1400 31032 phpreu 33523 poimirlem26 33565 indexa 33658 evth2f 39488 fvelrnbf 39491 evthf 39500 eliin2f 39601 stoweidlem34 40569 ovnlerp 41097 |
Copyright terms: Public domain | W3C validator |