Theorem rexralbidv 3207

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wral 3051  ∃wrex 3060

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 3052  df-rex 3061

This theorem is referenced by:  freq1  5621  rexfiuz  15366  cau3lem  15373  caubnd2  15376  climi  15526  rlimi  15529  o1lo1  15553  2clim  15588  lo1le  15668  caucvgrlem  15689  caurcvgr  15690  caucvgb  15696  vdwlem10  17010  vdwlem13  17013  pmatcollpw2lem  22715  neiptopnei  23070  lmcvg  23200  lmss  23236  elpt  23510  elptr  23511  txlm  23586  tsmsi  24072  ustuqtop4  24183  isucn  24216  isucn2  24217  ucnima  24219  metcnpi  24483  metcnpi2  24484  metucn  24510  xrge0tsms  24774  elcncf  24833  cncfi  24838  lmmcvg  25213  lhop1  25971  ulmval  26341  ulmi  26347  ulmcaulem  26355  ulmdvlem3  26363  pntibnd  27556  pntlem3  27572  pntleml  27574  axtgcont1  28447  perpln1  28689  perpln2  28690  isperp  28691  brbtwn  28878  uvtx01vtx  29376  isgrpo  30478  ubthlem3  30853  ubth  30854  hcau  31165  hcaucvg  31167  hlimi  31169  hlimconvi  31172  hlim2  31173  elcnop  31838  elcnfn  31863  cnopc  31894  cnfnc  31911  lnopcon  32016  lnfncon  32037  riesz1  32046  xrge0tsmsd  33056  signsply0  34583  unblimceq0  36525  cvgcau  45517  limcleqr  45673  addlimc  45677  0ellimcdiv  45678  climd  45701  climisp  45775  lmbr3  45776  climrescn  45777  climxrrelem  45778  climxrre  45779  xlimpnfxnegmnf  45843  xlimxrre  45860  xlimmnf  45870  xlimpnf  45871  xlimmnfmpt  45872  xlimpnfmpt  45873  dfxlim2  45877  cncfshift  45903  cncfperiod  45908  ioodvbdlimc1lem1  45960  ioodvbdlimc1lem2  45961  ioodvbdlimc2lem  45963  fourierdlem68  46203  fourierdlem87  46222  fourierdlem103  46238  fourierdlem104  46239  etransclem48  46311