Theorem r19.42v 3161

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 3159	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑) ↔ (∃𝑥 ∈ 𝐴 𝜓 ∧ 𝜑))
2		ancom 460	. . 3 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑))
3	2	rexbii 3076	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑))
4		ancom 460	. 2 ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜓 ∧ 𝜑))
5	1, 3, 4	3bitr4i 303	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓))

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

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 3054

This theorem is referenced by:  ceqsrexbv  3611  ceqsrex2v  3613  2reuswap  3706  2reuswap2  3707  2reu5  3718  2rmoswap  3721  dfiun2g  4980  iunrab  5001  iunin2  5020  iundif2  5023  reusv2lem4  5340  iunopab  5502  cnvuni  5829  elidinxp  5995  xpdifid  6117  dfpo2  6244  elunirn  7187  f1oiso  7288  oprabrexex2  7913  oeeu  8521  trcl  9624  dfac5lem2  10018  axgroth4  10726  rexuz2  12800  4fvwrd4  13551  cshwsexaOLD  14731  divalglem10  16313  divalgb  16315  lsmelval2  20989  tgcmp  23286  hauscmplem  23291  unisngl  23412  xkobval  23471  txtube  23525  txcmplem1  23526  txkgen  23537  xkococnlem  23544  mbfaddlem  25559  mbfsup  25563  elaa  26222  dchrisumlem3  27400  elold  27783  0reno  28366  colperpexlem3  28677  midex  28682  iscgra1  28755  ax5seg  28883  edglnl  29088  usgr2pth0  29710  hhcmpl  31144  sumdmdii  32359  reuxfrdf  32435  unipreima  32587  fpwrelmapffslem  32676  elirng  33659  esumfsup  34043  reprdifc  34601  bnj168  34703  bnj1398  35007  cvmliftlem15  35281  ellines  36136  bj-elsngl  36952  bj-dfmpoa  37102  ptrecube  37610  cnambfre  37658  islshpat  39006  lfl1dim  39110  glbconxN  39367  3dim0  39446  2dim  39459  1dimN  39460  islpln5  39524  islvol5  39568  dalem20  39682  lhpex2leN  40002  mapdval4N  41621  rexrabdioph  42777  rmxdioph  42999  expdiophlem1  43004  imaiun1  43634  coiun1  43635  ismnuprim  44277  prmunb2  44294  fourierdlem48  46145  2reuimp0  47108  2reuimp  47109  wtgoldbnnsum4prm  47796  bgoldbnnsum3prm  47798  dfvopnbgr2  47847  stgredgiun  47952  islindeps2  48478  isldepslvec2  48480  sepnsepolem1  48916