Theorem 2ralbidv 3227

Description: Formula-building rule for restricted universal quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.) (Revised by Szymon Jaroszewicz, 16-Mar-2007.)

Hypothesis

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

Assertion

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

Distinct variable groups:   𝜑,𝑥   𝜑,𝑦

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

Proof of Theorem 2ralbidv

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wral 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3068

This theorem is referenced by:  3ralbidv  3230  6ralbidv  3232  cbvral3vw  3249  cbvral6vw  3251  cbvral3v  3378  rspc6v  3656  ralxpxfr2d  3659  poeq1  5610  soeq1  5629  isoeq1  7353  isoeq2  7354  isoeq3  7355  fnmpoovd  8128  xpord3inddlem  8195  smoeq  8406  xpf1o  9205  nqereu  10998  dedekind  11453  dedekindle  11454  seqcaopr2  14089  wrd2ind  14771  addcn2  15640  mulcn2  15642  mreexexd  17706  catlid  17741  catrid  17742  isfunc  17928  funcres2b  17961  isfull  17977  isfth  17981  fullres2c  18006  isnat  18015  evlfcl  18292  uncfcurf  18309  isprs  18367  isdrs  18371  ispos  18384  istos  18488  isdlat  18592  ismgmhm  18734  issubmgm  18740  sgrp1  18767  ismhm  18820  issubm  18838  sgrp2nmndlem4  18963  isnsg  19195  isghm  19255  isghmOLD  19256  isga  19331  pmtrdifwrdel  19527  sylow2blem2  19663  efglem  19758  efgi  19761  efgredlemb  19788  efgred  19790  frgpuplem  19814  iscmn  19831  ring1  20333  isirred  20445  rnghmval  20466  isrnghm  20467  islmod  20884  lmodlema  20885  lssset  20954  islssd  20956  islmhm  21049  islmhm2  21060  isobs  21763  dmatel  22520  dmatmulcl  22527  scmateALT  22539  mdetunilem3  22641  mdetunilem4  22642  mdetunilem9  22647  cpmatel  22738  chpscmat  22869  hausnei2  23382  dfconn2  23448  llyeq  23499  nllyeq  23500  isucn2  24309  iducn  24313  ispsmet  24335  ismet  24354  isxmet  24355  metucn  24605  ngptgp  24670  nlmvscnlem1  24728  xmetdcn2  24878  addcnlem  24905  elcncf  24934  ipcnlem1  25298  cfili  25321  c1lip1  26056  aalioulem5  26396  aalioulem6  26397  aaliou  26398  aaliou2  26400  aaliou2b  26401  ulmcau  26456  ulmdvlem3  26463  cxpcn3lem  26808  mpodvdsmulf1o  27255  dvdsmulf1o  27257  chpdifbndlem2  27616  pntrsumbnd2  27629  addsprop  28027  negsprop  28085  istrkgb  28481  axtgsegcon  28490  axtg5seg  28491  axtgpasch  28493  axtgeucl  28498  iscgrg  28538  isismt  28560  isperp2  28741  f1otrg  28897  axcontlem10  29006  axcontlem12  29008  iscusgredg  29458  isgrpo  30529  isablo  30578  vacn  30726  smcnlem  30729  lnoval  30784  islno  30785  isphg  30849  ajmoi  30890  ajval  30893  adjmo  31864  elcnop  31889  ellnop  31890  elunop  31904  elhmop  31905  elcnfn  31914  ellnfn  31915  adjeu  31921  adjval  31922  adj1  31965  adjeq  31967  cnlnadjlem9  32107  cnlnadjeu  32110  cnlnssadj  32112  isst  32245  ishst  32246  cdj1i  32465  cdj3i  32473  resspos  32939  resstos  32940  ismnt  32956  mgcval  32960  isomnd  33051  isslmd  33181  slmdlema  33182  isorng  33294  prmidlval  33430  isprmidl  33431  isrprm  33510  qqhucn  33938  ismntop  33972  axtgupdim2ALTV  34645  txpconn  35200  nn0prpw  36289  heicant  37615  equivbnd  37750  isismty  37761  heibor1lem  37769  iccbnd  37800  isass  37806  elghomlem1OLD  37845  elghomlem2OLD  37846  isrngohom  37925  iscom2  37955  pridlval  37993  ispridl  37994  isdmn3  38034  inecmo  38311  islfl  39016  isopos  39136  psubspset  39701  islaut  40040  ispautN  40056  ltrnset  40075  isltrn  40076  istrnN  40114  istendo  40717  sticksstones1  42103  sticksstones2  42104  sticksstones3  42105  sticksstones8  42110  sticksstones10  42112  sticksstones11  42113  sticksstones12a  42114  sticksstones15  42118  sn-isghm  42628  clsk1independent  44008  sprsymrelfolem2  47367  sprsymrelfo  47371  reuopreuprim  47400  dmatALTbasel  48131  lindslinindsimp2  48192  lmod1  48221  isnrm4  48610  iscnrm4  48634  isthinc  48688  thincciso  48716