New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > 19.42v | GIF version |
Description: Special case of Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
19.42v | ⊢ (∃x(φ ∧ ψ) ↔ (φ ∧ ∃xψ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1619 | . 2 ⊢ Ⅎxφ | |
2 | 1 | 19.42 1880 | 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: exdistr 1906 19.42vv 1907 19.42vvv 1908 4exdistr 1911 cbvex2 2005 2sb5 2112 2sb5rf 2117 rexcom4a 2880 ceqsex2 2896 reuind 3040 2reu5lem3 3044 sbccomlem 3117 elpw1 4145 eluni1g 4173 opkelopkabg 4246 otkelins2kg 4254 eqvinop 4607 setconslem6 4737 dmopabss 4917 dmopab3 4918 dmcosseq 4974 coass 5098 dmoprab 5575 dmoprabss 5576 fnoprabg 5586 mptpreima 5683 dmmpt 5684 brsnsi2 5777 oqelins4 5795 addcfnex 5825 lecex 6116 ceex 6175 nmembers1lem1 6269 dmfrec 6317 |
Copyright terms: Public domain | W3C validator |