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 347 | . 2 ⊢ (𝑥 = 𝐴 → ((𝜑 ↔ 𝜓) ↔ (𝜒 ↔ 𝜃))) |
4 | vtoclbg.3 | . 2 ⊢ (𝜑 ↔ 𝜓) | |
5 | 3, 4 | vtoclg 3565 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 = wceq 1528 ∈ wcel 2105 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-nf 1776 df-cleq 2811 df-clel 2890 |
This theorem is referenced by: alexeqg 3641 pm13.183 3656 pm13.183OLD 3657 sbc8g 3777 sbc2or 3778 sbccow 3792 sbcco 3795 sbc5 3797 sbcie2g 3808 eqsbc3 3814 eqsbc3OLD 3815 sbcng 3816 sbcimg 3817 sbcan 3818 sbcor 3819 sbcbig 3820 sbcal 3830 sbcex2 3831 sbcel1v 3836 sbcel1vOLD 3837 sbcreu 3856 csbiebg 3912 sbcel12 4357 sbceqg 4358 elpwgOLD 4545 preq12bg 4776 elintrabg 4880 sbcbr123 5111 inisegn0 5954 fsn2g 6892 funfvima3 6989 elixpsn 8489 ixpsnf1o 8490 domeng 8511 1sdom 8709 rankcf 10187 eldm3 32894 elima4 32916 brsset 33247 brbigcup 33256 elfix2 33262 elfunsg 33274 elsingles 33276 funpartlem 33300 ellines 33510 elhf2g 33534 cover2g 34871 sbcrexgOLD 39260 |
Copyright terms: Public domain | W3C validator |