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 3447

Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995.) Avoid ax-12 2179. (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 480	. . 3 ⊢ ((𝑥 = 𝐴 ∧ 𝜑) → 𝜓)
3	2	exlimiv 1937	. 2 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) → 𝜓)
4	1	biimprcd 253	. . . 4 ⊢ (𝜓 → (𝑥 = 𝐴 → 𝜑))
5	4	alrimiv 1934	. . 3 ⊢ (𝜓 → ∀𝑥(𝑥 = 𝐴 → 𝜑))
6		ceqsexv.1	. . . 4 ⊢ 𝐴 ∈ V
7	6	isseti 3415	. . 3 ⊢ ∃𝑥 𝑥 = 𝐴
8		exintr 1899	. . 3 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) → (∃𝑥 𝑥 = 𝐴 → ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)))
9	5, 7, 8	mpisyl 21	. 2 ⊢ (𝜓 → ∃𝑥(𝑥 = 𝐴 ∧ 𝜑))
10	3, 9	impbii 212	1 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∀wal 1540 = wceq 1542 ∃wex 1786 ∈ wcel 2114 Vcvv 3400

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116

This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1787 df-clel 2812

This theorem is referenced by: ceqsexv2d 3449 ceqsex2v 3451 ceqsex3v 3452 gencbvex 3456 euxfr2w 3624 euxfr2 3626 inuni 5221 eqvinop 5354 elvvv 5608 dmfco 6776 fndmdif 6831 fndmin 6834 fmptco 6913 abrexco 7026 uniuni 7515 elxp4 7665 elxp5 7666 brtpos2 7939 xpsnen 8662 xpcomco 8668 xpassen 8672 dfac5lem2 9636 cf0 9763 ltexprlem4 10551 pceu 16295 4sqlem12 16404 vdwapun 16422 gsumval3eu 19155 dprd2d2 19297 znleval 20385 metrest 23289 fmptcof2 30581 fpwrelmapffslem 30654 cusgredgex 32666 imaeqsexv 33276 dfdm5 33333 dfrn5 33334 elima4 33336 brtxp 33837 brpprod 33842 elfix 33860 dfiota3 33880 brimg 33894 brapply 33895 brsuccf 33898 funpartlem 33899 brrestrict 33906 dfrecs2 33907 dfrdg4 33908 lshpsmreu 36778 isopos 36849 islpln5 37204 islvol5 37248 cdlemftr3 38234 dibelval3 38816 dicelval3 38849 mapdpglem3 39344 hdmapglem7a 39596 diophrex 40209

W3C validator