Theorem rexralbidv 3201

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

Hypothesis

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

Assertion

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

Distinct variable groups:   𝜑,𝑥   𝜑,𝑦

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

Proof of Theorem rexralbidv

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wral 3044  ∃wrex 3053

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 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3045  df-rex 3054

This theorem is referenced by:  freq1  5598  rexfiuz  15290  cau3lem  15297  caubnd2  15300  climi  15452  rlimi  15455  o1lo1  15479  2clim  15514  lo1le  15594  caucvgrlem  15615  caurcvgr  15616  caucvgb  15622  vdwlem10  16937  vdwlem13  16940  pmatcollpw2lem  22697  neiptopnei  23052  lmcvg  23182  lmss  23218  elpt  23492  elptr  23493  txlm  23568  tsmsi  24054  ustuqtop4  24165  isucn  24198  isucn2  24199  ucnima  24201  metcnpi  24465  metcnpi2  24466  metucn  24492  xrge0tsms  24756  elcncf  24815  cncfi  24820  lmmcvg  25194  lhop1  25952  ulmval  26322  ulmi  26328  ulmcaulem  26336  ulmdvlem3  26344  pntibnd  27537  pntlem3  27553  pntleml  27555  axtgcont1  28448  perpln1  28690  perpln2  28691  isperp  28692  brbtwn  28879  uvtx01vtx  29377  isgrpo  30476  ubthlem3  30851  ubth  30852  hcau  31163  hcaucvg  31165  hlimi  31167  hlimconvi  31170  hlim2  31171  elcnop  31836  elcnfn  31861  cnopc  31892  cnfnc  31909  lnopcon  32014  lnfncon  32035  riesz1  32044  xrge0tsmsd  33045  signsply0  34535  unblimceq0  36488  cvgcau  45479  limcleqr  45635  addlimc  45639  0ellimcdiv  45640  climd  45663  climisp  45737  lmbr3  45738  climrescn  45739  climxrrelem  45740  climxrre  45741  xlimpnfxnegmnf  45805  xlimxrre  45822  xlimmnf  45832  xlimpnf  45833  xlimmnfmpt  45834  xlimpnfmpt  45835  dfxlim2  45839  cncfshift  45865  cncfperiod  45870  ioodvbdlimc1lem1  45922  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  fourierdlem68  46165  fourierdlem87  46184  fourierdlem103  46200  fourierdlem104  46201  etransclem48  46273