Theorem r19.42v 3276

Description: Restricted quantifier version of 19.42v 1958 (see also 19.42 2232). (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 3273	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑) ↔ (∃𝑥 ∈ 𝐴 𝜓 ∧ 𝜑))
2		ancom 460	. . 3 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑))
3	2	rexbii 3177	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑))
4		ancom 460	. 2 ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜓 ∧ 𝜑))
5	1, 3, 4	3bitr4i 302	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓))

Syntax hints:   ↔ wb 205   ∧ wa 395  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-rex 3069

This theorem is referenced by:  rexcom  3281  ceqsrexbv  3579  ceqsrex2v  3580  2reuswap  3676  2reuswap2  3677  2reu5  3688  2rmoswap  3691  iunrab  4978  iunin2  4996  iundif2  4999  reusv2lem4  5319  iunopab  5465  cnvuni  5784  elidinxp  5940  xpdifid  6060  dfpo2  6188  elunirn  7106  f1oiso  7202  oprabrexex2  7794  oeeu  8396  trcl  9417  dfac5lem2  9811  axgroth4  10519  rexuz2  12568  4fvwrd4  13305  cshwsexa  14465  divalglem10  16039  divalgb  16041  lsmelval2  20262  tgcmp  22460  hauscmplem  22465  unisngl  22586  xkobval  22645  txtube  22699  txcmplem1  22700  txkgen  22711  xkococnlem  22718  mbfaddlem  24729  mbfsup  24733  elaa  25381  dchrisumlem3  26544  colperpexlem3  26997  midex  27002  iscgra1  27075  ax5seg  27209  edglnl  27416  usgr2pth0  28034  hhcmpl  29463  sumdmdii  30678  reuxfrdf  30740  unipreima  30882  fpwrelmapffslem  30969  esumfsup  31938  reprdifc  32507  bnj168  32609  bnj1398  32914  cvmliftlem15  33160  elold  33980  ellines  34381  bj-elsngl  35085  bj-dfmpoa  35216  ptrecube  35704  cnambfre  35752  islshpat  36958  lfl1dim  37062  glbconxN  37319  3dim0  37398  2dim  37411  1dimN  37412  islpln5  37476  islvol5  37520  dalem20  37634  lhpex2leN  37954  mapdval4N  39573  rexrabdioph  40532  rmxdioph  40754  expdiophlem1  40759  imaiun1  41148  coiun1  41149  ismnuprim  41801  prmunb2  41818  fourierdlem48  43585  2reuimp0  44493  2reuimp  44494  wtgoldbnnsum4prm  45142  bgoldbnnsum3prm  45144  islindeps2  45712  isldepslvec2  45714  sepnsepolem1  46103