![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > brralrspcev | Structured version Visualization version GIF version |
Description: Restricted existential specialization with a restricted universal quantifier over a relation, closed form. (Contributed by AV, 20-Aug-2022.) |
Ref | Expression |
---|---|
brralrspcev | ⊢ ((𝐵 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝑌 𝐴𝑅𝐵) → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐴𝑅𝑥) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | breq2 4847 | . . 3 ⊢ (𝑥 = 𝐵 → (𝐴𝑅𝑥 ↔ 𝐴𝑅𝐵)) | |
2 | 1 | ralbidv 3167 | . 2 ⊢ (𝑥 = 𝐵 → (∀𝑦 ∈ 𝑌 𝐴𝑅𝑥 ↔ ∀𝑦 ∈ 𝑌 𝐴𝑅𝐵)) |
3 | 2 | rspcev 3497 | 1 ⊢ ((𝐵 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝑌 𝐴𝑅𝐵) → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐴𝑅𝑥) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 385 = wceq 1653 ∈ wcel 2157 ∀wral 3089 ∃wrex 3090 class class class wbr 4843 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2377 ax-ext 2777 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-clab 2786 df-cleq 2792 df-clel 2795 df-nfc 2930 df-ral 3094 df-rex 3095 df-rab 3098 df-v 3387 df-dif 3772 df-un 3774 df-in 3776 df-ss 3783 df-nul 4116 df-if 4278 df-sn 4369 df-pr 4371 df-op 4375 df-br 4844 |
This theorem is referenced by: axpre-sup 10278 fimaxre2 11261 supaddc 11282 supadd 11283 supmul1 11284 supmullem2 11286 supmul 11287 rpnnen1lem2 12061 iccsupr 12516 supicc 12574 supiccub 12575 supicclub 12576 flval3 12871 fsequb 13029 sqrlem3 14326 caubnd2 14438 caubnd 14439 lo1bdd2 14596 lo1bddrp 14597 climcnds 14921 ruclem12 15306 maxprmfct 15754 prmreclem1 15953 prmreclem6 15958 ramz 16062 pgpssslw 18342 gexex 18571 icccmplem2 22954 icccmplem3 22955 reconnlem2 22958 cnllycmp 23083 cncmet 23448 ivthlem2 23560 ivthlem3 23561 cniccbdd 23569 ovolunlem1 23605 ovoliunlem1 23610 ovoliun2 23614 ioombl1lem4 23669 uniioombllem2 23691 uniioombllem6 23696 mbfinf 23773 mbflimsup 23774 itg1climres 23822 itg2i1fseq 23863 itg2i1fseq2 23864 itg2cnlem1 23869 plyeq0lem 24307 ulmbdd 24493 mtestbdd 24500 iblulm 24502 emcllem6 25079 lgambdd 25115 ftalem3 25153 ubthlem2 28252 ubthlem3 28253 htthlem 28299 rge0scvg 30511 esumpcvgval 30656 oddpwdc 30932 mblfinlem3 33937 ismblfin 33939 itg2addnc 33952 ubelsupr 39939 rexabslelem 40388 limsupubuz 40689 liminfreuzlem 40778 dvdivbd 40882 sge0supre 41349 sge0rnbnd 41353 meaiuninc2 41442 hoidmvlelem1 41555 hoidmvlelem4 41558 smfinflem 41769 |
Copyright terms: Public domain | W3C validator |