Theorem rexralbidv 3040

Description: Formula-building rule for restricted quantifiers (deduction rule). (Contributed by NM, 28-Jan-2006.)

Hypothesis

Ref	Expression
2rexbidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
rexralbidv	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))

Distinct variable groups:   𝜑,𝑥   𝜑,𝑦

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

Proof of Theorem rexralbidv

Step	Hyp	Ref	Expression
1		2rexbidv.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	ralbidv 2969	. 2 ⊢ (𝜑 → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒))
3	2	rexbidv 3034	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 195  ∀wral 2896  ∃wrex 2897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-ral 2901  df-rex 2902

This theorem is referenced by:  freq1  5008  rexfiuz  13935  cau3lem  13942  caubnd2  13945  climi  14089  rlimi  14092  o1lo1  14116  2clim  14151  lo1le  14230  caucvgrlem  14251  caurcvgr  14252  caucvgb  14258  vdwlem10  15532  vdwlem13  15535  pmatcollpw2lem  20401  neiptopnei  20746  lmcvg  20876  lmss  20912  elpt  21185  elptr  21186  txlm  21261  tsmsi  21747  ustuqtop4  21858  isucn  21892  isucn2  21893  ucnima  21895  metcnpi  22159  metcnpi2  22160  metucn  22186  xrge0tsms  22445  elcncf  22500  cncfi  22505  lmmcvg  22867  lhop1  23581  ulmval  23938  ulmi  23944  ulmcaulem  23952  ulmdvlem3  23960  pntibnd  25082  pntlem3  25098  pntleml  25100  axtgcont1  25167  perpln1  25405  perpln2  25406  isperp  25407  brbtwn  25579  isgrpo  26735  ubthlem3  27112  ubth  27113  hcau  27425  hcaucvg  27427  hlimi  27429  hlimconvi  27432  hlim2  27433  elcnop  28100  elcnfn  28125  cnopc  28156  cnfnc  28173  lnopcon  28278  lnfncon  28299  riesz1  28308  xrge0tsmsd  29116  signsply0  29954  limcleqr  38711  addlimc  38715  0ellimcdiv  38716  climd  38739  cncfshift  38759  cncfperiod  38764  ioodvbdlimc1lem1  38821  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  fourierdlem68  39067  fourierdlem87  39086  fourierdlem103  39102  fourierdlem104  39103  etransclem48  39175