Theorem brralrspcev 5157

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 5101	. . 3 ⊢ (𝑥 = 𝐵 → (𝐴𝑅𝑥 ↔ 𝐴𝑅𝐵))
2	1	ralbidv 3158	. 2 ⊢ (𝑥 = 𝐵 → (∀𝑦 ∈ 𝑌 𝐴𝑅𝑥 ↔ ∀𝑦 ∈ 𝑌 𝐴𝑅𝐵))
3	2	rspcev 3575	1 ⊢ ((𝐵 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝑌 𝐴𝑅𝐵) → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐴𝑅𝑥)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3050  ∃wrex 3059   class class class wbr 5097

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  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-ral 3051  df-rex 3060  df-rab 3399  df-v 3441  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4285  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098

This theorem is referenced by:  axpre-sup  11082  fimaxre2  12089  supaddc  12111  supadd  12112  supmul1  12113  supmullem2  12115  supmul  12116  rpnnen1lem2  12892  iccsupr  13360  supicc  13419  supiccub  13420  supicclub  13421  flval3  13737  fsequb  13900  01sqrexlem3  15169  caubnd2  15283  caubnd  15284  lo1bdd2  15449  lo1bddrp  15450  climcnds  15776  ruclem12  16168  maxprmfct  16638  prmreclem1  16846  prmreclem6  16851  ramz  16955  pgpssslw  19545  gexex  19784  icccmplem2  24770  icccmplem3  24771  reconnlem2  24774  cnllycmp  24913  cncmet  25280  ivthlem2  25411  ivthlem3  25412  cniccbdd  25420  ovolunlem1  25456  ovoliunlem1  25461  ovoliun2  25465  ioombl1lem4  25520  uniioombllem2  25542  uniioombllem6  25547  mbfinf  25624  mbflimsup  25625  itg1climres  25673  itg2i1fseq  25714  itg2i1fseq2  25715  itg2cnlem1  25720  plyeq0lem  26173  ulmbdd  26365  mtestbdd  26372  iblulm  26374  emcllem6  26969  lgambdd  27005  ftalem3  27043  ubthlem2  30927  ubthlem3  30928  htthlem  30973  rge0scvg  34085  esumpcvgval  34214  oddpwdc  34490  mblfinlem3  37829  ismblfin  37831  itg2addnc  37844  ubelsupr  45302  rexabslelem  45699  limsupubuz  45994  liminfreuzlem  46083  dvdivbd  46204  sge0supre  46670  sge0rnbnd  46674  meaiuninc2  46763  hoidmvlelem1  46876  hoidmvlelem4  46879  smfinflem  47098