![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > vtoclbg | Structured version Visualization version GIF version |
Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 29-Apr-1994.) |
Ref | Expression |
---|---|
vtoclbg.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) |
vtoclbg.2 | ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃)) |
vtoclbg.3 | ⊢ (𝜑 ↔ 𝜓) |
Ref | Expression |
---|---|
vtoclbg | ⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vtoclbg.1 | . . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) | |
2 | vtoclbg.2 | . . 3 ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃)) | |
3 | 1, 2 | bibi12d 334 | . 2 ⊢ (𝑥 = 𝐴 → ((𝜑 ↔ 𝜓) ↔ (𝜒 ↔ 𝜃))) |
4 | vtoclbg.3 | . 2 ⊢ (𝜑 ↔ 𝜓) | |
5 | 3, 4 | vtoclg 3398 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 = wceq 1624 ∈ wcel 2131 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1863 ax-4 1878 ax-5 1980 ax-6 2046 ax-7 2082 ax-9 2140 ax-12 2188 ax-ext 2732 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1627 df-ex 1846 df-nf 1851 df-sb 2039 df-clab 2739 df-cleq 2745 df-clel 2748 df-v 3334 |
This theorem is referenced by: alexeqg 3463 pm13.183 3476 sbc8g 3576 sbc2or 3577 sbcco 3591 sbc5 3593 sbcie2g 3602 eqsbc3 3608 sbcng 3609 sbcimg 3610 sbcan 3611 sbcor 3612 sbcbig 3613 sbcal 3618 sbcex2 3619 sbcel1v 3628 sbcreu 3648 csbiebg 3689 sbcel12 4118 sbceqg 4119 elpwg 4302 snssgOLD 4453 preq12bg 4522 elintgOLD 4628 elintrabg 4633 sbcbr123 4850 opelresgOLD 5555 inisegn0 5647 funfvima3 6650 elixpsn 8105 ixpsnf1o 8106 domeng 8127 1sdom 8320 rankcf 9783 eldm3 31950 br1steqgOLD 31971 br2ndeqgOLD 31972 elima4 31976 brsset 32294 brbigcup 32303 elfix2 32309 elfunsg 32321 elsingles 32323 funpartlem 32347 ellines 32557 elhf2g 32581 cover2g 33814 sbcrexgOLD 37843 sbcangOLD 39233 sbcorgOLD 39234 sbcalgOLD 39246 sbcexgOLD 39247 sbcel12gOLD 39248 sbcel1gvOLD 39585 |
Copyright terms: Public domain | W3C validator |