Theorem r19.42v 3198

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401  ∃wrex 3090

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-rex 3091

This theorem is used by:  ceqsrexbv  3613  ceqsrex2v  3615  2reuswap  3707  2reuswap2  3708  2reu5  3719  2rmoswap  3722  dfiun2g  4991  iunrab  5014  iunin2  5032  iundif2  5035  reusv2lem4  5367  iunopab  5538  cnvuni  5873  elidinxp  6042  xpdifid  6165  xpdifcnvepel  6166  dfpo2  6306  elunirn  7265  f1oiso  7369  oprabrexex2  8000  oeeu  8626  trcl  9742  dfac5lem2  10216  axgroth4  10930  rexuz2  13039  4fvwrd4  13795  divalglem10  16587  divalgb  16589  lsmelval2  21375  tgcmp  23734  hauscmplem  23739  unisngl  23861  xkobval  23920  txtube  23974  txcmplem1  23975  txkgen  23986  xkococnlem  23993  mbfaddlem  25996  mbfsup  26000  elaa  26654  dchrisumlem3  27833  elold  28260  colperpexlem3  29223  midex  29228  iscgra1  29332  ax5seg  29531  edglnl  29736  usgr2pth0  30366  hhcmpl  31817  sumdmdii  33032  reuxfrdf  33144  unipreima  33294  fpwrelmapffslem  33380  elirng  34374  esumfsup  34758  reprdifc  35312  bnj168  35417  bnj1398  35720  cvmliftlem15  36187  ellines  37047  bj-elsngl  38011  bj-elinxp  38090  bj-dfmpoa  38182  ptrecube  38681  cnambfre  38729  islshpat  40217  lfl1dim  40321  glbconxN  40578  3dim0  40657  2dim  40670  1dimN  40671  islpln5  40735  islvol5  40779  dalem20  40893  lhpex2leN  41213  mapdval4N  42832  rexrabdioph  43944  rmxdioph  44166  expdiophlem1  44171  imaiun1  44794  coiun1  44795  ismnuprim  45421  prmunb2  45438  fourierdlem48  47306  2reuimp0  48327  2reuimp  48328  wtgoldbnnsum4prm  49042  bgoldbnnsum3prm  49044  dfvopnbgr2  49093  stgredgiun  49198  islindeps2  49737  isldepslvec2  49739  sepnsepolem1  50178