Theorem brralrspcev 5207

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107  ∀wral 3062  ∃wrex 3071   class class class wbr 5147

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148

This theorem is referenced by:  axpre-sup  11160  fimaxre2  12155  supaddc  12177  supadd  12178  supmul1  12179  supmullem2  12181  supmul  12182  rpnnen1lem2  12957  iccsupr  13415  supicc  13474  supiccub  13475  supicclub  13476  flval3  13776  fsequb  13936  01sqrexlem3  15187  caubnd2  15300  caubnd  15301  lo1bdd2  15464  lo1bddrp  15465  climcnds  15793  ruclem12  16180  maxprmfct  16642  prmreclem1  16845  prmreclem6  16850  ramz  16954  pgpssslw  19475  gexex  19713  icccmplem2  24321  icccmplem3  24322  reconnlem2  24325  cnllycmp  24454  cncmet  24821  ivthlem2  24951  ivthlem3  24952  cniccbdd  24960  ovolunlem1  24996  ovoliunlem1  25001  ovoliun2  25005  ioombl1lem4  25060  uniioombllem2  25082  uniioombllem6  25087  mbfinf  25164  mbflimsup  25165  itg1climres  25214  itg2i1fseq  25255  itg2i1fseq2  25256  itg2cnlem1  25261  plyeq0lem  25706  ulmbdd  25892  mtestbdd  25899  iblulm  25901  emcllem6  26485  lgambdd  26521  ftalem3  26559  ubthlem2  30102  ubthlem3  30103  htthlem  30148  rge0scvg  32867  esumpcvgval  33014  oddpwdc  33291  mblfinlem3  36465  ismblfin  36467  itg2addnc  36480  ubelsupr  43637  rexabslelem  44063  limsupubuz  44364  liminfreuzlem  44453  dvdivbd  44574  sge0supre  45040  sge0rnbnd  45044  meaiuninc2  45133  hoidmvlelem1  45246  hoidmvlelem4  45249  smfinflem  45468