New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > 19.41v | GIF version |
Description: Special case of Theorem 19.41 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
19.41v | ⊢ (∃x(φ ∧ ψ) ↔ (∃xφ ∧ ψ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1619 | . 2 ⊢ Ⅎxψ | |
2 | 1 | 19.41 1879 | 1 ⊢ (∃x(φ ∧ ψ) ↔ (∃xφ ∧ ψ)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 176 ∧ wa 358 ∃wex 1541 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 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: 19.41vv 1902 19.41vvv 1903 19.41vvvv 1904 eeeanv 1914 gencbvex 2901 euxfr 3022 euind 3023 elpw11c 4147 elpw121c 4148 elpw131c 4149 elpw141c 4150 elpw151c 4151 elpw161c 4152 elpw171c 4153 elpw181c 4154 elpw191c 4155 elpw1101c 4156 elpw1111c 4157 eluni1g 4172 opkelcokg 4261 opkelimagekg 4271 dfimak2 4298 insklem 4304 ndisjrelk 4323 dfpw2 4327 dfaddc2 4381 dfnnc2 4395 elsuc 4413 nnsucelrlem1 4424 ltfinex 4464 ssfin 4470 eqpwrelk 4478 eqpw1relk 4479 ncfinraiselem2 4480 ncfinlowerlem1 4482 eqtfinrelk 4486 evenfinex 4503 oddfinex 4504 evenodddisjlem1 4515 nnadjoinlem1 4519 nnpweqlem1 4522 srelk 4524 sfintfinlem1 4531 tfinnnlem1 4533 spfinex 4537 vfinspsslem1 4550 dfop2lem1 4573 opeq 4619 opabn0 4716 setconslem1 4731 setconslem2 4732 setconslem3 4733 setconslem7 4737 df1st2 4738 dfswap2 4741 eliunxp 4821 dmuni 4914 elimapw11c 4948 dmres 4986 rnuni 5038 dminss 5041 imainss 5042 ssrnres 5059 cnvresima 5077 resco 5085 rnco 5087 coass 5097 df2nd2 5111 f11o 5315 dmsi 5519 rnoprab 5576 brimage 5793 dmtxp 5802 txpcofun 5803 addcfnex 5824 brpprod 5839 dmpprod 5840 pw1fnf1o 5855 fundmen 6043 ceexlem1 6173 el2c 6191 taddc 6229 tcfnex 6244 csucex 6259 addccan2nclem1 6263 nchoicelem11 6299 nchoicelem16 6304 |
Copyright terms: Public domain | W3C validator |