|   | 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 3360 with a disjoint variable condition, which does not require ax-13 2376. For a version not dependent on ax-11 2156 and ax-12, see cbvrexvw 3237. (Contributed by FL, 27-Apr-2008.) Avoid ax-10 2140, ax-13 2376. (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 1856 | . . . 4 ⊢ Ⅎ𝑦 ¬ 𝜑 | 
| 5 | cbvrexfw.4 | . . . . 5 ⊢ Ⅎ𝑥𝜓 | |
| 6 | 5 | nfn 1856 | . . . 4 ⊢ Ⅎ𝑥 ¬ 𝜓 | 
| 7 | cbvrexfw.5 | . . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
| 8 | 7 | notbid 318 | . . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓)) | 
| 9 | 1, 2, 4, 6, 8 | cbvralfw 3303 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑦 ∈ 𝐴 ¬ 𝜓) | 
| 10 | ralnex 3071 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑) | |
| 11 | ralnex 3071 | . . 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 1782 Ⅎwnfc 2889 ∀wral 3060 ∃wrex 3069 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-11 2156 ax-12 2176 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-ex 1779 df-nf 1783 df-clel 2815 df-nfc 2891 df-ral 3061 df-rex 3070 | 
| This theorem is referenced by: cbvrexw 3306 reusv2lem4 5400 reusv2 5402 nnwof 12957 cbviunf 32569 ac6sf2 32635 dfimafnf 32647 aciunf1lem 32673 bnj1400 34850 phpreu 37612 poimirlem26 37654 indexa 37741 evth2f 45025 fvelrnbf 45028 evthf 45037 eliin2f 45114 stoweidlem34 46054 ovnlerp 46582 | 
| Copyright terms: Public domain | W3C validator |