![]() |
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 2172. (Revised by Gino Giotto, 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 1846 | . . 3 ⊢ (∀𝑥(𝑥 = 𝐴 → ¬ 𝜑) ↔ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) | |
2 | ceqsexv.1 | . . . 4 ⊢ 𝐴 ∈ V | |
3 | ceqsexv.2 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
4 | 3 | notbid 318 | . . . 4 ⊢ (𝑥 = 𝐴 → (¬ 𝜑 ↔ ¬ 𝜓)) |
5 | 2, 4 | ceqsalv 3480 | . . 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 205 ∧ wa 397 ∀wal 1540 = wceq 1542 ∃wex 1782 ∈ wcel 2107 Vcvv 3444 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-clel 2811 |
This theorem is referenced by: ceqsexv2d 3496 ceqsex2v 3498 ceqsex3v 3499 gencbvex 3503 euxfr2w 3679 euxfr2 3681 inuni 5301 eqvinop 5445 elvvv 5708 dmfco 6938 fndmdif 6993 fndmin 6996 fmptco 7076 abrexco 7192 imaeqsexv 7309 imaeqexov 7593 uniuni 7697 elxp4 7860 elxp5 7861 brtpos2 8164 xpsnen 9002 xpcomco 9009 xpassen 9013 brttrcl2 9655 dfac5lem2 10065 cf0 10192 ltexprlem4 10980 pceu 16723 4sqlem12 16833 vdwapun 16851 gsumval3eu 19686 dprd2d2 19828 znleval 20977 metrest 23896 sleadd1 27320 addsunif 27332 addsasslem1 27333 addsasslem2 27334 fmptcof2 31619 fpwrelmapffslem 31696 cusgredgex 33772 dfdm5 34403 dfrn5 34404 elima4 34406 brtxp 34511 brpprod 34516 elfix 34534 dfiota3 34554 brimg 34568 brapply 34569 brsuccf 34572 funpartlem 34573 brrestrict 34580 dfrecs2 34581 dfrdg4 34582 lshpsmreu 37617 isopos 37688 islpln5 38044 islvol5 38088 cdlemftr3 39074 dibelval3 39656 dicelval3 39689 mapdpglem3 40184 hdmapglem7a 40436 diophrex 41141 |
Copyright terms: Public domain | W3C validator |