Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > cbvexv1 | Structured version Visualization version GIF version |
Description: Version of cbvex 2408 with a disjoint variable condition, which does not require ax-13 2381. See cbvexvw 2035 for a version with two disjoint variable conditions, requiring fewer axioms, and cbvexv 2410 for another variant. (Contributed by BJ, 31-May-2019.) |
Ref | Expression |
---|---|
cbvalv1.nf1 | ⊢ Ⅎ𝑦𝜑 |
cbvalv1.nf2 | ⊢ Ⅎ𝑥𝜓 |
cbvalv1.1 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
cbvexv1 | ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbvalv1.nf1 | . . . . 5 ⊢ Ⅎ𝑦𝜑 | |
2 | 1 | nfn 1848 | . . . 4 ⊢ Ⅎ𝑦 ¬ 𝜑 |
3 | cbvalv1.nf2 | . . . . 5 ⊢ Ⅎ𝑥𝜓 | |
4 | 3 | nfn 1848 | . . . 4 ⊢ Ⅎ𝑥 ¬ 𝜓 |
5 | cbvalv1.1 | . . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
6 | 5 | notbid 319 | . . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓)) |
7 | 2, 4, 6 | cbvalv1 2352 | . . 3 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓) |
8 | 7 | notbii 321 | . 2 ⊢ (¬ ∀𝑥 ¬ 𝜑 ↔ ¬ ∀𝑦 ¬ 𝜓) |
9 | df-ex 1772 | . 2 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑) | |
10 | df-ex 1772 | . 2 ⊢ (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓) | |
11 | 8, 9, 10 | 3bitr4i 304 | 1 ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∀wal 1526 ∃wex 1771 Ⅎwnf 1775 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-11 2151 ax-12 2167 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-ex 1772 df-nf 1776 |
This theorem is referenced by: sb8ev 2365 exsb 2369 mof 2640 euf 2654 clelab 2955 issetf 3505 eqvincf 3640 rexab2 3688 rexab2OLD 3689 euabsn 4654 eluniab 4841 cbvopab1 5130 cbvopab1g 5131 cbvopab2 5132 cbvopab1s 5133 axrep1 5182 axrep2 5184 axrep4 5186 opeliunxp 5612 dfdmf 5758 dfrnf 5813 elrnmpt1 5823 cbvoprab1 7230 cbvoprab2 7231 opabex3d 7655 opabex3rd 7656 opabex3 7657 zfcndrep 10024 fsum2dlem 15113 fprod2dlem 15322 bnj1146 31962 bnj607 32087 bnj1228 32180 poimirlem26 34799 sbcexf 35274 elunif 41150 stoweidlem46 42208 opeliun2xp 44309 |
Copyright terms: Public domain | W3C validator |