Theorem rexralbidv 3198

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wral 3047  ∃wrex 3056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-ral 3048  df-rex 3057

This theorem is referenced by:  freq1  5581  rexfiuz  15255  cau3lem  15262  caubnd2  15265  climi  15417  rlimi  15420  o1lo1  15444  2clim  15479  lo1le  15559  caucvgrlem  15580  caurcvgr  15581  caucvgb  15587  vdwlem10  16902  vdwlem13  16905  pmatcollpw2lem  22692  neiptopnei  23047  lmcvg  23177  lmss  23213  elpt  23487  elptr  23488  txlm  23563  tsmsi  24049  ustuqtop4  24159  isucn  24192  isucn2  24193  ucnima  24195  metcnpi  24459  metcnpi2  24460  metucn  24486  xrge0tsms  24750  elcncf  24809  cncfi  24814  lmmcvg  25188  lhop1  25946  ulmval  26316  ulmi  26322  ulmcaulem  26330  ulmdvlem3  26338  pntibnd  27531  pntlem3  27547  pntleml  27549  axtgcont1  28446  perpln1  28688  perpln2  28689  isperp  28690  brbtwn  28877  uvtx01vtx  29375  isgrpo  30477  ubthlem3  30852  ubth  30853  hcau  31164  hcaucvg  31166  hlimi  31168  hlimconvi  31171  hlim2  31172  elcnop  31837  elcnfn  31862  cnopc  31893  cnfnc  31910  lnopcon  32015  lnfncon  32036  riesz1  32045  xrge0tsmsd  33042  signsply0  34564  unblimceq0  36551  cvgcau  45598  limcleqr  45752  addlimc  45756  0ellimcdiv  45757  climd  45780  climisp  45854  lmbr3  45855  climrescn  45856  climxrrelem  45857  climxrre  45858  xlimpnfxnegmnf  45922  xlimxrre  45939  xlimmnf  45949  xlimpnf  45950  xlimmnfmpt  45951  xlimpnfmpt  45952  dfxlim2  45956  cncfshift  45982  cncfperiod  45987  ioodvbdlimc1lem1  46039  ioodvbdlimc1lem2  46040  ioodvbdlimc2lem  46042  fourierdlem68  46282  fourierdlem87  46301  fourierdlem103  46317  fourierdlem104  46318  etransclem48  46390