Theorem r19.42v 3170

Description: Restricted quantifier version of 19.42v 1953 (see also 19.42 2237). (Contributed by NM, 27-May-1998.)

Assertion

Ref	Expression
r19.42v	⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem r19.42v

Step	Hyp	Ref	Expression
1		r19.41v 3168	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑) ↔ (∃𝑥 ∈ 𝐴 𝜓 ∧ 𝜑))
2		ancom 460	. . 3 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑))
3	2	rexbii 3077	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑))
4		ancom 460	. 2 ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜓 ∧ 𝜑))
5	1, 3, 4	3bitr4i 303	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓))

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wrex 3054

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3055

This theorem is referenced by:  rexcomOLD  3268  ceqsrexbv  3625  ceqsrex2v  3627  2reuswap  3720  2reuswap2  3721  2reu5  3732  2rmoswap  3735  dfiun2g  4997  iunrab  5019  iunin2  5038  iundif2  5041  reusv2lem4  5359  iunopab  5522  iunopabOLD  5523  cnvuni  5853  elidinxp  6018  xpdifid  6144  dfpo2  6272  elunirn  7228  f1oiso  7329  oprabrexex2  7960  oeeu  8570  trcl  9688  dfac5lem2  10084  axgroth4  10792  rexuz2  12865  4fvwrd4  13616  cshwsexaOLD  14797  divalglem10  16379  divalgb  16381  lsmelval2  20999  tgcmp  23295  hauscmplem  23300  unisngl  23421  xkobval  23480  txtube  23534  txcmplem1  23535  txkgen  23546  xkococnlem  23553  mbfaddlem  25568  mbfsup  25572  elaa  26231  dchrisumlem3  27409  elold  27788  0reno  28355  colperpexlem3  28666  midex  28671  iscgra1  28744  ax5seg  28872  edglnl  29077  usgr2pth0  29702  hhcmpl  31136  sumdmdii  32351  reuxfrdf  32427  unipreima  32574  fpwrelmapffslem  32662  elirng  33688  esumfsup  34067  reprdifc  34625  bnj168  34727  bnj1398  35031  cvmliftlem15  35292  ellines  36147  bj-elsngl  36963  bj-dfmpoa  37113  ptrecube  37621  cnambfre  37669  islshpat  39017  lfl1dim  39121  glbconxN  39379  3dim0  39458  2dim  39471  1dimN  39472  islpln5  39536  islvol5  39580  dalem20  39694  lhpex2leN  40014  mapdval4N  41633  rexrabdioph  42789  rmxdioph  43012  expdiophlem1  43017  imaiun1  43647  coiun1  43648  ismnuprim  44290  prmunb2  44307  fourierdlem48  46159  2reuimp0  47119  2reuimp  47120  wtgoldbnnsum4prm  47807  bgoldbnnsum3prm  47809  dfvopnbgr2  47857  stgredgiun  47961  islindeps2  48476  isldepslvec2  48478  sepnsepolem1  48914