Theorem r19.42v 3171

Description: Restricted quantifier version of 19.42v 1960 (see also 19.42 2248). (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 3169	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑) ↔ (∃𝑥 ∈ 𝐴 𝜓 ∧ 𝜑))
2		ancom 461	. . 3 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑))
3	2	rexbii 3086	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑))
4		ancom 461	. 2 ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜓 ∧ 𝜑))
5	1, 3, 4	3bitr4i 304	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓))

Syntax hints:   ↔ wb 207   ∧ wa 396  ∃wrex 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-rex 3064

This theorem is referenced by:  ceqsrexbv  3594  ceqsrex2v  3596  2reuswap  3687  2reuswap2  3688  2reu5  3699  2rmoswap  3702  dfiun2g  4960  iunrab  4983  iunin2  5001  iundif2  5004  reusv2lem4  5331  iunopab  5502  cnvuni  5829  elidinxp  5997  xpdifid  6120  dfpo2  6248  elunirn  7196  f1oiso  7296  oprabrexex2  7921  oeeu  8530  trcl  9641  dfac5lem2  10038  axgroth4  10747  rexuz2  12841  4fvwrd4  13594  divalglem10  16363  divalgb  16365  lsmelval2  21076  tgcmp  23385  hauscmplem  23390  unisngl  23511  xkobval  23570  txtube  23624  txcmplem1  23625  txkgen  23636  xkococnlem  23643  mbfaddlem  25646  mbfsup  25650  elaa  26301  dchrisumlem3  27473  elold  27870  colperpexlem3  28819  midex  28824  iscgra1  28897  ax5seg  29026  edglnl  29231  usgr2pth0  29852  hhcmpl  31290  sumdmdii  32505  reuxfrdf  32579  unipreima  32736  fpwrelmapffslem  32825  elirng  33879  esumfsup  34263  reprdifc  34820  bnj168  34922  bnj1398  35225  cvmliftlem15  35535  ellines  36389  bj-elsngl  37330  bj-dfmpoa  37485  ptrecube  37996  cnambfre  38044  islshpat  39518  lfl1dim  39622  glbconxN  39879  3dim0  39958  2dim  39971  1dimN  39972  islpln5  40036  islvol5  40080  dalem20  40194  lhpex2leN  40514  mapdval4N  42133  rexrabdioph  43248  rmxdioph  43470  expdiophlem1  43475  imaiun1  44104  coiun1  44105  ismnuprim  44747  prmunb2  44764  fourierdlem48  46605  2reuimp0  47585  2reuimp  47586  wtgoldbnnsum4prm  48301  bgoldbnnsum3prm  48303  dfvopnbgr2  48352  stgredgiun  48457  islindeps2  48982  isldepslvec2  48984  sepnsepolem1  49420