![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cbvrexfw | Structured version Visualization version GIF version |
Description: Rule used to change bound variables, using implicit substitution. Version of cbvrexf 3359 with a disjoint variable condition, which does not require ax-13 2375. For a version not dependent on ax-11 2155 and ax-12, see cbvrexvw 3236. (Contributed by FL, 27-Apr-2008.) Avoid ax-10 2139, ax-13 2375. (Revised by GG, 10-Jan-2024.) |
Ref | Expression |
---|---|
cbvrexfw.1 | ⊢ Ⅎ𝑥𝐴 |
cbvrexfw.2 | ⊢ Ⅎ𝑦𝐴 |
cbvrexfw.3 | ⊢ Ⅎ𝑦𝜑 |
cbvrexfw.4 | ⊢ Ⅎ𝑥𝜓 |
cbvrexfw.5 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
cbvrexfw | ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbvrexfw.1 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
2 | cbvrexfw.2 | . . . 4 ⊢ Ⅎ𝑦𝐴 | |
3 | cbvrexfw.3 | . . . . 5 ⊢ Ⅎ𝑦𝜑 | |
4 | 3 | nfn 1855 | . . . 4 ⊢ Ⅎ𝑦 ¬ 𝜑 |
5 | cbvrexfw.4 | . . . . 5 ⊢ Ⅎ𝑥𝜓 | |
6 | 5 | nfn 1855 | . . . 4 ⊢ Ⅎ𝑥 ¬ 𝜓 |
7 | cbvrexfw.5 | . . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
8 | 7 | notbid 318 | . . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓)) |
9 | 1, 2, 4, 6, 8 | cbvralfw 3302 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑦 ∈ 𝐴 ¬ 𝜓) |
10 | ralnex 3070 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑) | |
11 | ralnex 3070 | . . 3 ⊢ (∀𝑦 ∈ 𝐴 ¬ 𝜓 ↔ ¬ ∃𝑦 ∈ 𝐴 𝜓) | |
12 | 9, 10, 11 | 3bitr3i 301 | . 2 ⊢ (¬ ∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∃𝑦 ∈ 𝐴 𝜓) |
13 | 12 | con4bii 321 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 Ⅎwnf 1780 Ⅎwnfc 2888 ∀wral 3059 ∃wrex 3068 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-11 2155 ax-12 2175 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-ex 1777 df-nf 1781 df-clel 2814 df-nfc 2890 df-ral 3060 df-rex 3069 |
This theorem is referenced by: cbvrexw 3305 reusv2lem4 5407 reusv2 5409 nnwof 12954 cbviunf 32576 ac6sf2 32642 dfimafnf 32653 aciunf1lem 32679 bnj1400 34828 phpreu 37591 poimirlem26 37633 indexa 37720 evth2f 44953 fvelrnbf 44956 evthf 44965 eliin2f 45044 stoweidlem34 45990 ovnlerp 46518 |
Copyright terms: Public domain | W3C validator |