Theorem brralrspcev 5173

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567   ∈ wcel 2149  ∀wral 3085  ∃wrex 3095   class class class wbr 5111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3423  df-v 3463  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4491  df-sn 4593  df-pr 4595  df-op 4599  df-br 5112

This theorem is referenced by:  axpre-sup  11154  fimaxre2  12160  supaddc  12182  supadd  12183  supmul1  12184  supmullem2  12186  supmul  12187  rpnnen1lem2  13001  iccsupr  13469  supicc  13528  supiccub  13529  supicclub  13530  flval3  13848  fsequb  14011  01sqrexlem3  15295  caubnd2  15409  caubnd  15410  lo1bdd2  15575  lo1bddrp  15576  climcnds  15905  ruclem12  16297  maxprmfct  16768  prmreclem1  16976  prmreclem6  16981  ramz  17085  pgpssslw  19684  gexex  19923  icccmplem2  24950  icccmplem3  24951  reconnlem2  24954  cnllycmp  25084  cncmet  25450  ivthlem2  25580  ivthlem3  25581  cniccbdd  25589  ovolunlem1  25625  ovoliunlem1  25630  ovoliun2  25634  ioombl1lem4  25689  uniioombllem2  25711  uniioombllem6  25716  mbfinf  25793  mbflimsup  25794  itg1climres  25842  itg2i1fseq  25883  itg2i1fseq2  25884  itg2cnlem1  25889  plyeq0lem  26336  ulmbdd  26527  mtestbdd  26534  iblulm  26536  emcllem6  27131  lgambdd  27167  ftalem3  27205  ubthlem2  31164  ubthlem3  31165  htthlem  31210  rge0scvg  34284  esumpcvgval  34413  oddpwdc  34689  mblfinlem3  38233  ismblfin  38235  itg2addnc  38248  ubelsupr  45667  rexabslelem  46059  limsupubuz  46354  liminfreuzlem  46443  dvdivbd  46564  sge0supre  47030  sge0rnbnd  47034  meaiuninc2  47123  hoidmvlelem1  47236  hoidmvlelem4  47239  smfinflem  47458