|   | 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 3361 with a disjoint variable condition, which does not require ax-13 2377. For a version not dependent on ax-11 2157 and ax-12, see cbvrexvw 3238. (Contributed by FL, 27-Apr-2008.) Avoid ax-10 2141, ax-13 2377. (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 1857 | . . . 4 ⊢ Ⅎ𝑦 ¬ 𝜑 | 
| 5 | cbvrexfw.4 | . . . . 5 ⊢ Ⅎ𝑥𝜓 | |
| 6 | 5 | nfn 1857 | . . . 4 ⊢ Ⅎ𝑥 ¬ 𝜓 | 
| 7 | cbvrexfw.5 | . . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
| 8 | 7 | notbid 318 | . . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓)) | 
| 9 | 1, 2, 4, 6, 8 | cbvralfw 3304 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑦 ∈ 𝐴 ¬ 𝜓) | 
| 10 | ralnex 3072 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑) | |
| 11 | ralnex 3072 | . . 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 1783 Ⅎwnfc 2890 ∀wral 3061 ∃wrex 3070 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-11 2157 ax-12 2177 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-ex 1780 df-nf 1784 df-clel 2816 df-nfc 2892 df-ral 3062 df-rex 3071 | 
| This theorem is referenced by: cbvrexw 3307 reusv2lem4 5401 reusv2 5403 nnwof 12956 cbviunf 32568 ac6sf2 32634 dfimafnf 32646 aciunf1lem 32672 bnj1400 34849 phpreu 37611 poimirlem26 37653 indexa 37740 evth2f 45020 fvelrnbf 45023 evthf 45032 eliin2f 45109 stoweidlem34 46049 ovnlerp 46577 | 
| Copyright terms: Public domain | W3C validator |