Theorem brralrspcev 5208

Description: Restricted existential specialization with a restricted universal quantifier over a relation, closed form. (Contributed by AV, 20-Aug-2022.)

Assertion

Ref	Expression
brralrspcev	⊢ ((𝐵 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝑌 𝐴𝑅𝐵) → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐴𝑅𝑥)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵,𝑦   𝑥,𝑅   𝑥,𝑋   𝑥,𝑌

Allowed substitution hints:   𝐴(𝑦)   𝑅(𝑦)   𝑋(𝑦)   𝑌(𝑦)

Proof of Theorem brralrspcev

Step	Hyp	Ref	Expression
1		breq2 5152	. . 3 ⊢ (𝑥 = 𝐵 → (𝐴𝑅𝑥 ↔ 𝐴𝑅𝐵))
2	1	ralbidv 3177	. 2 ⊢ (𝑥 = 𝐵 → (∀𝑦 ∈ 𝑌 𝐴𝑅𝑥 ↔ ∀𝑦 ∈ 𝑌 𝐴𝑅𝐵))
3	2	rspcev 3612	1 ⊢ ((𝐵 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝑌 𝐴𝑅𝐵) → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐴𝑅𝑥)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  ∀wral 3061  ∃wrex 3070   class class class wbr 5148

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149

This theorem is referenced by:  axpre-sup  11166  fimaxre2  12161  supaddc  12183  supadd  12184  supmul1  12185  supmullem2  12187  supmul  12188  rpnnen1lem2  12963  iccsupr  13421  supicc  13480  supiccub  13481  supicclub  13482  flval3  13782  fsequb  13942  01sqrexlem3  15193  caubnd2  15306  caubnd  15307  lo1bdd2  15470  lo1bddrp  15471  climcnds  15799  ruclem12  16186  maxprmfct  16648  prmreclem1  16851  prmreclem6  16856  ramz  16960  pgpssslw  19484  gexex  19723  icccmplem2  24346  icccmplem3  24347  reconnlem2  24350  cnllycmp  24479  cncmet  24846  ivthlem2  24976  ivthlem3  24977  cniccbdd  24985  ovolunlem1  25021  ovoliunlem1  25026  ovoliun2  25030  ioombl1lem4  25085  uniioombllem2  25107  uniioombllem6  25112  mbfinf  25189  mbflimsup  25190  itg1climres  25239  itg2i1fseq  25280  itg2i1fseq2  25281  itg2cnlem1  25286  plyeq0lem  25731  ulmbdd  25917  mtestbdd  25924  iblulm  25926  emcllem6  26512  lgambdd  26548  ftalem3  26586  ubthlem2  30162  ubthlem3  30163  htthlem  30208  rge0scvg  32998  esumpcvgval  33145  oddpwdc  33422  mblfinlem3  36619  ismblfin  36621  itg2addnc  36634  ubelsupr  43792  rexabslelem  44213  limsupubuz  44514  liminfreuzlem  44603  dvdivbd  44724  sge0supre  45190  sge0rnbnd  45194  meaiuninc2  45283  hoidmvlelem1  45396  hoidmvlelem4  45399  smfinflem  45618