![]() |
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.) |
Ref | Expression |
---|---|
ceqsexv.1 | ⊢ 𝐴 ∈ V |
ceqsexv.2 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
ceqsexv | ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1956 | . 2 ⊢ Ⅎ𝑥𝜓 | |
2 | ceqsexv.1 | . 2 ⊢ 𝐴 ∈ V | |
3 | ceqsexv.2 | . 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
4 | 1, 2, 3 | ceqsex 3345 | 1 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 383 = wceq 1596 ∃wex 1817 ∈ wcel 2103 Vcvv 3304 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1835 ax-4 1850 ax-5 1952 ax-6 2018 ax-7 2054 ax-9 2112 ax-12 2160 ax-ext 2704 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1599 df-ex 1818 df-nf 1823 df-sb 2011 df-clab 2711 df-cleq 2717 df-clel 2720 df-v 3306 |
This theorem is referenced by: ceqsexv2d 3347 ceqsex3v 3350 gencbvex 3354 euxfr2 3497 inuni 4931 eqvinop 5059 elvvv 5287 dmfco 6386 fndmdif 6436 fndmin 6439 fmptco 6511 abrexco 6617 uniuni 7088 elxp4 7227 elxp5 7228 opabex3d 7262 opabex3 7263 fsplit 7402 brtpos2 7478 mapsnen 8151 xpsnen 8160 xpcomco 8166 xpassen 8170 dfac5lem1 9059 dfac5lem2 9060 dfac5lem3 9061 cf0 9186 ltexprlem4 9974 pceu 15674 4sqlem12 15783 vdwapun 15801 gsumval3eu 18426 dprd2d2 18564 znleval 20026 metrest 22451 fmptcof2 29687 fpwrelmapffslem 29737 dfdm5 31902 dfrn5 31903 elima4 31905 brtxp 32214 brpprod 32219 elfix 32237 dffix2 32239 sscoid 32247 dfiota3 32257 brimg 32271 brapply 32272 brsuccf 32275 funpartlem 32276 brrestrict 32283 dfrecs2 32284 dfrdg4 32285 lshpsmreu 34816 isopos 34887 islpln5 35241 islvol5 35285 pmapglb 35476 polval2N 35612 cdlemftr3 36272 dibelval3 36855 dicelval3 36888 mapdpglem3 37383 hdmapglem7a 37638 diophrex 37758 mapsnend 39807 opeliun2xp 42538 |
Copyright terms: Public domain | W3C validator |