Theorem brralrspcev 5117

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1531   ∈ wcel 2108  ∀wral 3136  ∃wrex 3137   class class class wbr 5057

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-br 5058

This theorem is referenced by:  axpre-sup  10583  fimaxre2  11578  supaddc  11600  supadd  11601  supmul1  11602  supmullem2  11604  supmul  11605  rpnnen1lem2  12368  iccsupr  12822  supicc  12878  supiccub  12879  supicclub  12880  flval3  13177  fsequb  13335  sqrlem3  14596  caubnd2  14709  caubnd  14710  lo1bdd2  14873  lo1bddrp  14874  climcnds  15198  ruclem12  15586  maxprmfct  16045  prmreclem1  16244  prmreclem6  16249  ramz  16353  pgpssslw  18731  gexex  18965  icccmplem2  23423  icccmplem3  23424  reconnlem2  23427  cnllycmp  23552  cncmet  23917  ivthlem2  24045  ivthlem3  24046  cniccbdd  24054  ovolunlem1  24090  ovoliunlem1  24095  ovoliun2  24099  ioombl1lem4  24154  uniioombllem2  24176  uniioombllem6  24181  mbfinf  24258  mbflimsup  24259  itg1climres  24307  itg2i1fseq  24348  itg2i1fseq2  24349  itg2cnlem1  24354  plyeq0lem  24792  ulmbdd  24978  mtestbdd  24985  iblulm  24987  emcllem6  25570  lgambdd  25606  ftalem3  25644  ubthlem2  28640  ubthlem3  28641  htthlem  28686  rge0scvg  31185  esumpcvgval  31330  oddpwdc  31605  mblfinlem3  34923  ismblfin  34925  itg2addnc  34938  ubelsupr  41268  rexabslelem  41682  limsupubuz  41984  liminfreuzlem  42073  dvdivbd  42198  sge0supre  42662  sge0rnbnd  42666  meaiuninc2  42755  hoidmvlelem1  42868  hoidmvlelem4  42871  smfinflem  43082