ceqsexv - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ceqsexv		Structured version Visualization version GIF version

Theorem ceqsexv 3515

Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995.) Avoid ax-12 2166. (Revised by Gino Giotto, 12-Oct-2024.) (Proof shortened by Wolf Lammen, 22-Jan-2025.)

**Hypotheses**
Ref	Expression
ceqsexv.1	⊢ 𝐴 ∈ V
ceqsexv.2	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

**Assertion**
Ref	Expression
ceqsexv	⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓)

Distinct variable groups: 𝑥,𝐴 𝜓,𝑥 Allowed substitution hint: 𝜑(𝑥)

**Proof of Theorem ceqsexv**
Step	Hyp	Ref	Expression
1		alinexa 1837	. . 3 ⊢ (∀𝑥(𝑥 = 𝐴 → ¬ 𝜑) ↔ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑))
2		ceqsexv.1	. . . 4 ⊢ 𝐴 ∈ V
3		ceqsexv.2	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	3	notbid 317	. . . 4 ⊢ (𝑥 = 𝐴 → (¬ 𝜑 ↔ ¬ 𝜓))
5	2, 4	ceqsalv 3501	. . 3 ⊢ (∀𝑥(𝑥 = 𝐴 → ¬ 𝜑) ↔ ¬ 𝜓)
6	1, 5	bitr3i 276	. 2 ⊢ (¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ ¬ 𝜓)
7	6	con4bii 320	1 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 394 ∀wal 1531 = wceq 1533 ∃wex 1773 ∈ wcel 2098 Vcvv 3463

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100

This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-clel 2802

This theorem is referenced by: ceqsexv2d 3518 ceqsex2v 3520 ceqsex3v 3521 gencbvex 3525 euxfr2w 3707 euxfr2 3709 inuni 5340 eqvinop 5483 elvvv 5747 dmfco 6989 fndmdif 7046 fndmin 7049 fmptco 7134 abrexco 7250 imaeqsexv 7367 imaeqexov 7656 uniuni 7762 elxp4 7928 elxp5 7929 brtpos2 8236 xpsnen 9078 xpcomco 9085 xpassen 9089 brttrcl2 9737 dfac5lem2 10147 cf0 10274 ltexprlem4 11062 pceu 16814 4sqlem12 16924 vdwapun 16942 gsumval3eu 19863 dprd2d2 20005 znleval 21492 metrest 24451 sleadd1 27924 addsuniflem 27936 addsasslem1 27938 addsasslem2 27939 mulsuniflem 28071 addsdilem1 28073 addsdilem2 28074 mulsasslem1 28085 mulsasslem2 28086 renegscl 28270 readdscl 28271 remulscl 28274 fmptcof2 32488 fpwrelmapffslem 32559 cusgredgex 34788 dfdm5 35425 dfrn5 35426 elima4 35428 brtxp 35533 brpprod 35538 elfix 35556 dfiota3 35576 brimg 35590 brapply 35591 brsuccf 35594 funpartlem 35595 brrestrict 35602 dfrecs2 35603 dfrdg4 35604 lshpsmreu 38637 isopos 38708 islpln5 39064 islvol5 39108 cdlemftr3 40094 dibelval3 40676 dicelval3 40709 mapdpglem3 41204 hdmapglem7a 41456 diophrex 42260

W3C validator

	
		OSZAR »