Theorem reximdv2 3164

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 17-Sep-2003.)

Hypothesis

Ref	Expression
reximdv2.1	⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) → (𝑥 ∈ 𝐵 ∧ 𝜒)))

Assertion

Ref	Expression
reximdv2	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐵 𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)   𝐵(𝑥)

Proof of Theorem reximdv2

Step	Hyp	Ref	Expression
1		reximdv2.1	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) → (𝑥 ∈ 𝐵 ∧ 𝜒)))
2	1	eximdv 1920	. 2 ⊢ (𝜑 → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜒)))
3		df-rex 3071	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓))
4		df-rex 3071	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝜒 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜒))
5	2, 3, 4	3imtr4g 295	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ∧ wa 396  ∃wex 1781   ∈ wcel 2106  ∃wrex 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-ex 1782  df-rex 3071

This theorem is referenced by:  reximdvai  3165  reximssdv  3172  ssrexv  4051  ssimaex  6976  nnsuc  7872  oaass  8560  omeulem1  8581  ssnnfi  9168  ssnnfiOLD  9169  findcard3  9284  findcard3OLD  9285  unfilem1  9309  epfrs  9725  alephval3  10104  isfin7-2  10390  fpwwe2lem12  10636  inawinalem  10683  ico0  13369  ioc0  13370  r19.2uz  15297  climrlim2  15490  prmdvdsncoprmbd  16662  iserodd  16767  ramub2  16946  prmgaplem6  16988  ablfaclem3  19956  unitgrp  20196  restnlly  22985  llyrest  22988  nllyrest  22989  llyidm  22991  nllyidm  22992  cnpflfi  23502  cnextcn  23570  ivthlem3  24969  dvfsumrlim  25547  lgsquadlem2  26881  oppperpex  28001  outpasch  28003  ushgredgedg  28483  ushgredgedgloop  28485  cusgrfilem2  28710  nsgqusf1olem2  32520  ghmquskerlem2  32525  ssmxidl  32585  cmppcmp  32833  eulerpartlemgvv  33370  eulerpartlemgh  33372  fnrelpredd  34087  erdszelem7  34183  rellysconn  34237  ivthALT  35215  fnessref  35237  phpreu  36467  poimirlem26  36509  itg2gt0cn  36538  frinfm  36598  sstotbnd2  36637  heiborlem3  36676  isdrngo3  36822  dihjat1lem  40294  dvh1dim  40308  dochsatshp  40317  mapdpglem2  40539  prjspreln0  41352  pellexlem5  41561  pell14qrss1234  41584  pell1qrss14  41596  lnr2i  41848  hbtlem6  41861  dflim5  42069  tfsconcatrn  42082  naddgeoa  42135  mnuop3d  43020  fvelsetpreimafv  46045  opnneir  47529