Theorem reximdv2 3043

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

Syntax hints:   → wi 4   ∧ wa 383  ∃wex 1744   ∈ wcel 2030  ∃wrex 2942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879

This theorem depends on definitions:  df-bi 197  df-ex 1745  df-rex 2947

This theorem is referenced by:  ssrexv  3700  ssimaex  6302  nnsuc  7124  oaass  7686  omeulem1  7707  ssnnfi  8220  findcard3  8244  unfilem1  8265  epfrs  8645  alephval3  8971  isfin7-2  9256  fin1a2lem6  9265  fpwwe2lem12  9501  fpwwe2lem13  9502  inawinalem  9549  ico0  12259  ioc0  12260  r19.2uz  14135  climrlim2  14322  iserodd  15587  ramub2  15765  prmgaplem6  15807  pgpssslw  18075  efgrelexlemb  18209  ablfaclem3  18532  unitgrp  18713  lspsneq  19170  lbsextlem4  19209  neissex  20979  iscnp4  21115  nlly2i  21327  llynlly  21328  restnlly  21333  llyrest  21336  nllyrest  21337  llyidm  21339  nllyidm  21340  qtophmeo  21668  cnpflfi  21850  cnextcn  21918  ivthlem3  23268  ovolicc2lem5  23335  dvfsumrlim  23839  itgsubst  23857  lgsquadlem2  25151  footex  25658  opphllem1  25684  oppperpex  25690  outpasch  25692  ushgredgedg  26166  ushgredgedgloop  26168  cusgrfilem2  26408  cmppcmp  30053  eulerpartlemgvv  30566  eulerpartlemgh  30568  erdszelem7  31305  rellysconn  31359  trpredrec  31862  ivthALT  32455  fnessref  32477  phpreu  33523  poimirlem26  33565  itg2gt0cn  33595  frinfm  33660  sstotbnd2  33703  heiborlem3  33742  isdrngo3  33888  dihjat1lem  37034  dvh1dim  37048  dochsatshp  37057  lcfl6  37106  mapdval2N  37236  mapdpglem2  37279  hdmaprnlem10N  37468  pellexlem5  37714  pell14qrss1234  37737  pell1qrss14  37749  pellfundglb  37766  lnr2i  38003  hbtlem6  38016