Theorem brralrspcev 5095

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∀wral 3070  ∃wrex 3071   class class class wbr 5035

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-ral 3075  df-rex 3076  df-v 3411  df-un 3865  df-sn 4526  df-pr 4528  df-op 4532  df-br 5036

This theorem is referenced by:  axpre-sup  10634  fimaxre2  11628  supaddc  11649  supadd  11650  supmul1  11651  supmullem2  11653  supmul  11654  rpnnen1lem2  12422  iccsupr  12879  supicc  12938  supiccub  12939  supicclub  12940  flval3  13239  fsequb  13397  sqrlem3  14657  caubnd2  14770  caubnd  14771  lo1bdd2  14934  lo1bddrp  14935  climcnds  15259  ruclem12  15647  maxprmfct  16110  prmreclem1  16312  prmreclem6  16317  ramz  16421  pgpssslw  18811  gexex  19046  icccmplem2  23529  icccmplem3  23530  reconnlem2  23533  cnllycmp  23662  cncmet  24027  ivthlem2  24157  ivthlem3  24158  cniccbdd  24166  ovolunlem1  24202  ovoliunlem1  24207  ovoliun2  24211  ioombl1lem4  24266  uniioombllem2  24288  uniioombllem6  24293  mbfinf  24370  mbflimsup  24371  itg1climres  24419  itg2i1fseq  24460  itg2i1fseq2  24461  itg2cnlem1  24466  plyeq0lem  24911  ulmbdd  25097  mtestbdd  25104  iblulm  25106  emcllem6  25690  lgambdd  25726  ftalem3  25764  ubthlem2  28758  ubthlem3  28759  htthlem  28804  rge0scvg  31424  esumpcvgval  31569  oddpwdc  31844  mblfinlem3  35402  ismblfin  35404  itg2addnc  35417  ubelsupr  42050  rexabslelem  42449  limsupubuz  42749  liminfreuzlem  42838  dvdivbd  42959  sge0supre  43422  sge0rnbnd  43426  meaiuninc2  43515  hoidmvlelem1  43628  hoidmvlelem4  43631  smfinflem  43842