| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ceqsexv | Structured version Visualization version GIF version | ||
| Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995.) Avoid ax-12 2177. (Revised by GG, 12-Oct-2024.) (Proof shortened by Wolf Lammen, 22-Jan-2025.) |
| Ref | Expression |
|---|---|
| ceqsexv.1 | ⊢ 𝐴 ∈ V |
| ceqsexv.2 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
| Ref | Expression |
|---|---|
| ceqsexv | ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | alinexa 1843 | . . 3 ⊢ (∀𝑥(𝑥 = 𝐴 → ¬ 𝜑) ↔ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) | |
| 2 | ceqsexv.1 | . . . 4 ⊢ 𝐴 ∈ V | |
| 3 | ceqsexv.2 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
| 4 | 3 | notbid 318 | . . . 4 ⊢ (𝑥 = 𝐴 → (¬ 𝜑 ↔ ¬ 𝜓)) |
| 5 | 2, 4 | ceqsalv 3521 | . . 3 ⊢ (∀𝑥(𝑥 = 𝐴 → ¬ 𝜑) ↔ ¬ 𝜓) |
| 6 | 1, 5 | bitr3i 277 | . 2 ⊢ (¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ ¬ 𝜓) |
| 7 | 6 | con4bii 321 | 1 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∀wal 1538 = wceq 1540 ∃wex 1779 ∈ wcel 2108 Vcvv 3480 |
| 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 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-clel 2816 |
| This theorem is referenced by: ceqsexv2dOLD 3534 ceqsex2v 3536 ceqsex3v 3537 gencbvex 3541 euxfr2w 3726 euxfr2 3728 inuni 5350 eqvinop 5492 elvvv 5761 dmfco 7005 fndmdif 7062 fndmin 7065 fmptco 7149 abrexco 7264 imaeqsexvOLD 7383 imaeqexov 7671 uniuni 7782 elxp4 7944 elxp5 7945 brtpos2 8257 xpsnen 9095 xpcomco 9102 xpassen 9106 brttrcl2 9754 dfac5lem2 10164 cf0 10291 ltexprlem4 11079 pceu 16884 4sqlem12 16994 vdwapun 17012 gsumval3eu 19922 dprd2d2 20064 znleval 21573 metrest 24537 sleadd1 28022 addsuniflem 28034 addsasslem1 28036 addsasslem2 28037 mulsuniflem 28175 addsdilem1 28177 addsdilem2 28178 mulsasslem1 28189 mulsasslem2 28190 renegscl 28430 readdscl 28431 remulscl 28434 fmptcof2 32667 fpwrelmapffslem 32743 cusgredgex 35127 dfdm5 35773 dfrn5 35774 elima4 35776 brtxp 35881 brpprod 35886 elfix 35904 dfiota3 35924 brimg 35938 brapply 35939 brsuccf 35942 funpartlem 35943 brrestrict 35950 dfrecs2 35951 dfrdg4 35952 lshpsmreu 39110 isopos 39181 islpln5 39537 islvol5 39581 cdlemftr3 40567 dibelval3 41149 dicelval3 41182 mapdpglem3 41677 hdmapglem7a 41929 diophrex 42786 |
| Copyright terms: Public domain | W3C validator |