Theorem r19.42v 3285

Description: Restricted quantifier version of 19.42v 1912 (see also 19.42 2169). (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 3282	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑) ↔ (∃𝑥 ∈ 𝐴 𝜓 ∧ 𝜑))
2		ancom 453	. . 3 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑))
3	2	rexbii 3188	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑))
4		ancom 453	. 2 ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜓 ∧ 𝜑))
5	1, 3, 4	3bitr4i 295	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓))

Syntax hints:   ↔ wb 198   ∧ wa 387  ∃wrex 3083

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-rex 3088

This theorem is referenced by:  rexcom  3290  ceqsrexbv  3558  ceqsrex2v  3559  2reuswap  3643  2reuswap2  3644  2reu5  3652  2rmoswap  3655  iunrab  4838  iunin2  4855  iundif2  4858  reusv2lem4  5151  iunopab  5294  cnvuni  5603  elidinxp  5753  xpdifid  5862  elunirn  6833  f1oiso  6925  oprabrexex2  7489  oeeu  8028  trcl  8962  dfac5lem2  9342  axgroth4  10050  rexuz2  12111  4fvwrd4  12841  cshwsexa  14046  divalglem10  15611  divalgb  15613  lsmelval2  19591  tgcmp  21725  hauscmplem  21730  unisngl  21851  xkobval  21910  txtube  21964  txcmplem1  21965  txkgen  21976  xkococnlem  21983  mbfaddlem  23976  mbfsup  23980  elaa  24620  dchrisumlem3  25781  colperpexlem3  26232  midex  26237  iscgra1  26310  ax5seg  26439  edglnl  26643  usgr2pth0  27266  hhcmpl  28768  sumdmdii  29985  unipreima  30167  fpwrelmapffslem  30241  esumfsup  31002  reprdifc  31575  bnj168  31677  bnj1398  31980  cvmliftlem15  32159  dfpo2  32540  ellines  33163  bj-elsngl  33827  bj-dfmpoa  33948  ptrecube  34362  cnambfre  34410  islshpat  35627  lfl1dim  35731  glbconxN  35988  3dim0  36067  2dim  36080  1dimN  36081  islpln5  36145  islvol5  36189  dalem20  36303  lhpex2leN  36623  mapdval4N  38242  rexrabdioph  38816  rmxdioph  39038  expdiophlem1  39043  imaiun1  39388  coiun1  39389  ismnuprim  40034  prmunb2  40088  fourierdlem48  41895  2reuimp0  42744  2reuimp  42745  wtgoldbnnsum4prm  43360  bgoldbnnsum3prm  43362  islindeps2  43930  isldepslvec2  43932