Theorem rexralbidv 3204

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 3161	. 2 ⊢ (𝜑 → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒))
3	2	rexbidv 3162	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 206  ∀wral 3052  ∃wrex 3062

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 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-ral 3053  df-rex 3063

This theorem is referenced by:  freq1  5599  rexfiuz  15283  cau3lem  15290  caubnd2  15293  climi  15445  rlimi  15448  o1lo1  15472  2clim  15507  lo1le  15587  caucvgrlem  15608  caurcvgr  15609  caucvgb  15615  vdwlem10  16930  vdwlem13  16933  pmatcollpw2lem  22733  neiptopnei  23088  lmcvg  23218  lmss  23254  elpt  23528  elptr  23529  txlm  23604  tsmsi  24090  ustuqtop4  24200  isucn  24233  isucn2  24234  ucnima  24236  metcnpi  24500  metcnpi2  24501  metucn  24527  xrge0tsms  24791  elcncf  24850  cncfi  24855  lmmcvg  25229  lhop1  25987  ulmval  26357  ulmi  26363  ulmcaulem  26371  ulmdvlem3  26379  pntibnd  27572  pntlem3  27588  pntleml  27590  axtgcont1  28552  perpln1  28794  perpln2  28795  isperp  28796  brbtwn  28984  uvtx01vtx  29482  isgrpo  30585  ubthlem3  30960  ubth  30961  hcau  31272  hcaucvg  31274  hlimi  31276  hlimconvi  31279  hlim2  31280  elcnop  31945  elcnfn  31970  cnopc  32001  cnfnc  32018  lnopcon  32123  lnfncon  32144  riesz1  32153  xrge0tsmsd  33167  signsply0  34729  unblimceq0  36729  cvgcau  45848  limcleqr  46002  addlimc  46006  0ellimcdiv  46007  climd  46030  climisp  46104  lmbr3  46105  climrescn  46106  climxrrelem  46107  climxrre  46108  xlimpnfxnegmnf  46172  xlimxrre  46189  xlimmnf  46199  xlimpnf  46200  xlimmnfmpt  46201  xlimpnfmpt  46202  dfxlim2  46206  cncfshift  46232  cncfperiod  46237  ioodvbdlimc1lem1  46289  ioodvbdlimc1lem2  46290  ioodvbdlimc2lem  46292  fourierdlem68  46532  fourierdlem87  46551  fourierdlem103  46567  fourierdlem104  46568  etransclem48  46640