Theorem r19.42v 3203

Description: Restricted quantifier version of 19.42v 1980 (see also 19.42 2278). (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 3201	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑) ↔ (∃𝑥 ∈ 𝐴 𝜓 ∧ 𝜑))
2		ancom 465	. . 3 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑))
3	2	rexbii 3118	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑))
4		ancom 465	. 2 ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜓 ∧ 𝜑))
5	1, 3, 4	3bitr4i 306	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓))

Syntax hints:   ↔ wb 209   ∧ wa 400  ∃wrex 3095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-rex 3096

This theorem is referenced by:  ceqsrexbv  3624  ceqsrex2v  3626  2reuswap  3718  2reuswap2  3719  2reu5  3730  2rmoswap  3733  dfiun2g  4998  iunrab  5021  iunin2  5039  iundif2  5042  reusv2lem4  5373  iunopab  5545  cnvuni  5877  elidinxp  6047  xpdifid  6166  xpdifcnvepel  6167  dfpo2  6298  elunirn  7250  f1oiso  7350  oprabrexex2  7975  oeeu  8589  trcl  9697  dfac5lem2  10108  axgroth4  10817  rexuz2  12923  4fvwrd4  13676  divalglem10  16460  divalgb  16462  lsmelval2  21184  tgcmp  23527  hauscmplem  23532  unisngl  23653  xkobval  23712  txtube  23766  txcmplem1  23767  txkgen  23778  xkococnlem  23785  mbfaddlem  25788  mbfsup  25792  elaa  26446  dchrisumlem3  27621  elold  28018  colperpexlem3  28972  midex  28977  iscgra1  29078  ax5seg  29229  edglnl  29434  usgr2pth0  30055  hhcmpl  31493  sumdmdii  32708  reuxfrdf  32778  unipreima  32929  fpwrelmapffslem  33018  elirng  34021  esumfsup  34405  reprdifc  34959  bnj168  35064  bnj1398  35367  cvmliftlem15  35723  ellines  36577  bj-elsngl  37526  bj-dfmpoa  37682  ptrecube  38193  cnambfre  38241  islshpat  39715  lfl1dim  39819  glbconxN  40076  3dim0  40155  2dim  40168  1dimN  40169  islpln5  40233  islvol5  40277  dalem20  40391  lhpex2leN  40711  mapdval4N  42330  rexrabdioph  43447  rmxdioph  43669  expdiophlem1  43674  imaiun1  44303  coiun1  44304  ismnuprim  44930  prmunb2  44947  fourierdlem48  46794  2reuimp0  47774  2reuimp  47775  wtgoldbnnsum4prm  48490  bgoldbnnsum3prm  48492  dfvopnbgr2  48541  stgredgiun  48646  islindeps2  49182  isldepslvec2  49184  sepnsepolem1  49619