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 3469

Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995.) Avoid ax-12 2173. (Revised by Gino Giotto, 12-Oct-2024.)

**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		ceqsexv.2	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
2	1	biimpa 476	. . 3 ⊢ ((𝑥 = 𝐴 ∧ 𝜑) → 𝜓)
3	2	exlimiv 1934	. 2 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) → 𝜓)
4	1	biimprcd 249	. . . 4 ⊢ (𝜓 → (𝑥 = 𝐴 → 𝜑))
5	4	alrimiv 1931	. . 3 ⊢ (𝜓 → ∀𝑥(𝑥 = 𝐴 → 𝜑))
6		ceqsexv.1	. . . 4 ⊢ 𝐴 ∈ V
7	6	isseti 3437	. . 3 ⊢ ∃𝑥 𝑥 = 𝐴
8		exintr 1896	. . 3 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) → (∃𝑥 𝑥 = 𝐴 → ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)))
9	5, 7, 8	mpisyl 21	. 2 ⊢ (𝜓 → ∃𝑥(𝑥 = 𝐴 ∧ 𝜑))
10	3, 9	impbii 208	1 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 ∀wal 1537 = wceq 1539 ∃wex 1783 ∈ wcel 2108 Vcvv 3422

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110

This theorem depends on definitions: df-bi 206 df-an 396 df-ex 1784 df-clel 2817

This theorem is referenced by: ceqsexv2d 3471 ceqsex2v 3473 ceqsex3v 3474 gencbvex 3478 euxfr2w 3650 euxfr2 3652 inuni 5262 eqvinop 5395 elvvv 5653 dmfco 6846 fndmdif 6901 fndmin 6904 fmptco 6983 abrexco 7099 uniuni 7590 elxp4 7743 elxp5 7744 brtpos2 8019 xpsnen 8796 xpcomco 8802 xpassen 8806 dfac5lem2 9811 cf0 9938 ltexprlem4 10726 pceu 16475 4sqlem12 16585 vdwapun 16603 gsumval3eu 19420 dprd2d2 19562 znleval 20674 metrest 23586 fmptcof2 30896 fpwrelmapffslem 30969 cusgredgex 32983 imaeqsexv 33593 dfdm5 33653 dfrn5 33654 elima4 33656 brttrcl2 33700 brtxp 34109 brpprod 34114 elfix 34132 dfiota3 34152 brimg 34166 brapply 34167 brsuccf 34170 funpartlem 34171 brrestrict 34178 dfrecs2 34179 dfrdg4 34180 lshpsmreu 37050 isopos 37121 islpln5 37476 islvol5 37520 cdlemftr3 38506 dibelval3 39088 dicelval3 39121 mapdpglem3 39616 hdmapglem7a 39868 diophrex 40513

W3C validator