Theorem reximdv2 3162

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 1918	. 2 ⊢ (𝜑 → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜒)))
3		df-rex 3069	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓))
4		df-rex 3069	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝜒 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜒))
5	2, 3, 4	3imtr4g 295	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ∧ wa 394  ∃wex 1779   ∈ wcel 2104  ∃wrex 3068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911

This theorem depends on definitions:  df-bi 206  df-ex 1780  df-rex 3069

This theorem is referenced by:  reximdvai  3163  reximssdv  3170  ssrexv  4050  ssimaex  6975  nnsuc  7875  oaass  8563  omeulem1  8584  ssnnfi  9171  ssnnfiOLD  9172  findcard3  9287  findcard3OLD  9288  unfilem1  9312  epfrs  9728  alephval3  10107  isfin7-2  10393  fpwwe2lem12  10639  inawinalem  10686  ico0  13374  ioc0  13375  r19.2uz  15302  climrlim2  15495  prmdvdsncoprmbd  16667  iserodd  16772  ramub2  16951  prmgaplem6  16993  ablfaclem3  19998  unitgrp  20274  restnlly  23206  llyrest  23209  nllyrest  23210  llyidm  23212  nllyidm  23213  cnpflfi  23723  cnextcn  23791  ivthlem3  25202  dvfsumrlim  25783  lgsquadlem2  27120  oppperpex  28271  outpasch  28273  ushgredgedg  28753  ushgredgedgloop  28755  cusgrfilem2  28980  nsgqusf1olem2  32799  ghmquskerlem2  32804  ssmxidl  32864  cmppcmp  33136  eulerpartlemgvv  33673  eulerpartlemgh  33675  fnrelpredd  34390  erdszelem7  34486  rellysconn  34540  ivthALT  35523  fnessref  35545  phpreu  36775  poimirlem26  36817  itg2gt0cn  36846  frinfm  36906  sstotbnd2  36945  heiborlem3  36984  isdrngo3  37130  dihjat1lem  40602  dvh1dim  40616  dochsatshp  40625  mapdpglem2  40847  prjspreln0  41653  pellexlem5  41873  pell14qrss1234  41896  pell1qrss14  41908  lnr2i  42160  hbtlem6  42173  dflim5  42381  tfsconcatrn  42394  naddgeoa  42447  mnuop3d  43332  fvelsetpreimafv  46353  opnneir  47626