New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > 19.42v | Unicode version |
Description: Special case of Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
19.42v |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1619 | . 2 | |
2 | 1 | 19.42 1880 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wb 176 wa 358 wex 1541 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-6 1729 ax-11 1746 |
This theorem depends on definitions: df-bi 177 df-an 360 df-ex 1542 df-nf 1545 |
This theorem is referenced by: exdistr 1906 19.42vv 1907 19.42vvv 1908 4exdistr 1911 cbvex2 2005 2sb5 2112 2sb5rf 2117 rexcom4a 2879 ceqsex2 2895 reuind 3039 2reu5lem3 3043 sbccomlem 3116 elpw1 4144 eluni1g 4172 opkelopkabg 4245 otkelins2kg 4253 eqvinop 4606 setconslem6 4736 dmopabss 4916 dmopab3 4917 dmcosseq 4973 coass 5097 dmoprab 5574 dmoprabss 5575 fnoprabg 5585 mptpreima 5682 dmmpt 5683 brsnsi2 5776 oqelins4 5794 addcfnex 5824 lecex 6115 ceex 6174 nmembers1lem1 6268 dmfrec 6316 |
Copyright terms: Public domain | W3C validator |