![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ceqsexv | Structured version Visualization version Unicode version |
Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995.) |
Ref | Expression |
---|---|
ceqsexv.1 |
![]() ![]() ![]() ![]() |
ceqsexv.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
ceqsexv |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1761 |
. 2
![]() ![]() ![]() ![]() | |
2 | ceqsexv.1 |
. 2
![]() ![]() ![]() ![]() | |
3 | ceqsexv.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | ceqsex 3083 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-10 1915 ax-12 1933 ax-ext 2431 |
This theorem depends on definitions: df-bi 189 df-an 373 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-clab 2438 df-cleq 2444 df-clel 2447 df-v 3047 |
This theorem is referenced by: ceqsexv2d 3085 ceqsex3v 3088 gencbvex 3092 sbhypf 3095 euxfr2 3223 inuni 4565 eqvinop 4686 dfid3 4750 opeliunxp 4886 elvvv 4894 imai 5180 coi1 5351 dmfco 5939 fndmdif 5986 fndmin 5989 fmptco 6056 abrexco 6149 uniuni 6600 elxp4 6737 elxp5 6738 opabex3d 6771 opabex3 6772 fsplit 6901 brtpos2 6979 mapsnen 7647 xpsnen 7656 xpcomco 7662 xpassen 7666 dfac5lem1 8554 dfac5lem2 8555 dfac5lem3 8556 cf0 8681 ltexprlem4 9464 pceu 14796 4sqlem12 14900 vdwapun 14924 gsumval3eu 17538 dprd2d2 17677 znleval 19125 metrest 21539 fmptcof2 28259 fpwrelmapffslem 28317 dfdm5 30418 dfrn5 30419 elima4 30421 nofulllem5 30595 brtxp 30647 brpprod 30652 elfix 30670 dffix2 30672 sscoid 30680 elfuns 30682 dfiota3 30690 brimg 30704 brapply 30705 brsuccf 30708 funpartlem 30709 brrestrict 30716 dfrecs2 30717 dfrdg4 30718 lshpsmreu 32675 isopos 32746 islpln5 33100 islvol5 33144 pmapglb 33335 polval2N 33471 cdlemftr3 34132 dibelval3 34715 dicelval3 34748 mapdpglem3 35243 hdmapglem7a 35498 diophrex 35618 mapsnend 37480 opeliun2xp 40167 |
Copyright terms: Public domain | W3C validator |