Theorem brralrspcev 5126

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537   ∈ wcel 2114  ∀wral 3138  ∃wrex 3139   class class class wbr 5066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067

This theorem is referenced by:  axpre-sup  10591  fimaxre2  11586  supaddc  11608  supadd  11609  supmul1  11610  supmullem2  11612  supmul  11613  rpnnen1lem2  12377  iccsupr  12831  supicc  12887  supiccub  12888  supicclub  12889  flval3  13186  fsequb  13344  sqrlem3  14604  caubnd2  14717  caubnd  14718  lo1bdd2  14881  lo1bddrp  14882  climcnds  15206  ruclem12  15594  maxprmfct  16053  prmreclem1  16252  prmreclem6  16257  ramz  16361  pgpssslw  18739  gexex  18973  icccmplem2  23431  icccmplem3  23432  reconnlem2  23435  cnllycmp  23560  cncmet  23925  ivthlem2  24053  ivthlem3  24054  cniccbdd  24062  ovolunlem1  24098  ovoliunlem1  24103  ovoliun2  24107  ioombl1lem4  24162  uniioombllem2  24184  uniioombllem6  24189  mbfinf  24266  mbflimsup  24267  itg1climres  24315  itg2i1fseq  24356  itg2i1fseq2  24357  itg2cnlem1  24362  plyeq0lem  24800  ulmbdd  24986  mtestbdd  24993  iblulm  24995  emcllem6  25578  lgambdd  25614  ftalem3  25652  ubthlem2  28648  ubthlem3  28649  htthlem  28694  rge0scvg  31192  esumpcvgval  31337  oddpwdc  31612  mblfinlem3  34946  ismblfin  34948  itg2addnc  34961  ubelsupr  41326  rexabslelem  41741  limsupubuz  42043  liminfreuzlem  42132  dvdivbd  42257  sge0supre  42720  sge0rnbnd  42724  meaiuninc2  42813  hoidmvlelem1  42926  hoidmvlelem4  42929  smfinflem  43140