Theorem brralrspcev 5170

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3045  ∃wrex 3054   class class class wbr 5110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111

This theorem is referenced by:  axpre-sup  11129  fimaxre2  12135  supaddc  12157  supadd  12158  supmul1  12159  supmullem2  12161  supmul  12162  rpnnen1lem2  12943  iccsupr  13410  supicc  13469  supiccub  13470  supicclub  13471  flval3  13784  fsequb  13947  01sqrexlem3  15217  caubnd2  15331  caubnd  15332  lo1bdd2  15497  lo1bddrp  15498  climcnds  15824  ruclem12  16216  maxprmfct  16686  prmreclem1  16894  prmreclem6  16899  ramz  17003  pgpssslw  19551  gexex  19790  icccmplem2  24719  icccmplem3  24720  reconnlem2  24723  cnllycmp  24862  cncmet  25229  ivthlem2  25360  ivthlem3  25361  cniccbdd  25369  ovolunlem1  25405  ovoliunlem1  25410  ovoliun2  25414  ioombl1lem4  25469  uniioombllem2  25491  uniioombllem6  25496  mbfinf  25573  mbflimsup  25574  itg1climres  25622  itg2i1fseq  25663  itg2i1fseq2  25664  itg2cnlem1  25669  plyeq0lem  26122  ulmbdd  26314  mtestbdd  26321  iblulm  26323  emcllem6  26918  lgambdd  26954  ftalem3  26992  ubthlem2  30807  ubthlem3  30808  htthlem  30853  rge0scvg  33946  esumpcvgval  34075  oddpwdc  34352  mblfinlem3  37660  ismblfin  37662  itg2addnc  37675  ubelsupr  45021  rexabslelem  45421  limsupubuz  45718  liminfreuzlem  45807  dvdivbd  45928  sge0supre  46394  sge0rnbnd  46398  meaiuninc2  46487  hoidmvlelem1  46600  hoidmvlelem4  46603  smfinflem  46822